ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple{i:l}
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), A:ecl-trans-tuple(ds; da).
ecl-trans-halt2(ds; da; A)  (event-info(ds;da) List)prop{i:l} 

latex

Definitions	ecl-trans-tuple{i:l}(ds; da), Knd, fpf(A; a.B(a)), x. t(x), Id, ecl-trans-halt2(ds; da; A), prop{i:l}, b, ecl-trans-h(v), ecl-trans-state(v; L), event-info(ds;da), x:A. B(x), t  T,
Lemmas	nat wf, event-info wf, ecl-trans-state wf, ecl-trans-h wf, assert wf, Id wf, fpf wf, Knd wf, ecl-trans-tuple wf